Combining and automating classical and non-classical logics in classical higher-order logics
Identifieur interne : 002738 ( Main/Exploration ); précédent : 002737; suivant : 002739Combining and automating classical and non-classical logics in classical higher-order logics
Auteurs : Christoph Benzmüller [États-Unis]Source :
- Annals of Mathematics and Artificial Intelligence [ 1012-2443 ] ; 2011-06-01.
English descriptors
- KwdEn :
Abstract
Abstract: Numerous classical and non-classical logics can be elegantly embedded in Church’s simple type theory, also known as classical higher-order logic. Examples include propositional and quantified multimodal logics, intuitionistic logics, logics for security, and logics for spatial reasoning. Furthermore, simple type theory is sufficiently expressive to model combinations of embedded logics and it has a well understood semantics. Off-the-shelf reasoning systems for simple type theory exist that can be uniformly employed for reasoning within and about embedded logics and logics combinations. In this article we focus on combinations of (quantified) epistemic and doxastic logics and study their application for modeling and automating the reasoning of rational agents. We present illustrating example problems and report on experiments with off-the-shelf higher-order automated theorem provers.
Url:
DOI: 10.1007/s10472-011-9249-7
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001794
- to stream Istex, to step Curation: 001775
- to stream Istex, to step Checkpoint: 000638
- to stream Main, to step Merge: 002780
- to stream Main, to step Curation: 002738
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Combining and automating classical and non-classical logics in classical higher-order logics</title><author><name sortKey="Benzmuller, Christoph" sort="Benzmuller, Christoph" uniqKey="Benzmuller C" first="Christoph" last="Benzmüller">Christoph Benzmüller</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:66DC056FECD94BC479D88167A3E49EDD4002FF46</idno><date when="2011" year="2011">2011</date><idno type="doi">10.1007/s10472-011-9249-7</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-VPX5CN5S-G/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001794</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001794</idno><idno type="wicri:Area/Istex/Curation">001775</idno><idno type="wicri:Area/Istex/Checkpoint">000638</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000638</idno><idno type="wicri:doubleKey">1012-2443:2011:Benzmuller C:combining:and:automating</idno><idno type="wicri:Area/Main/Merge">002780</idno><idno type="wicri:Area/Main/Curation">002738</idno><idno type="wicri:Area/Main/Exploration">002738</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Combining and automating classical and non-classical logics in classical higher-order logics</title><author><name sortKey="Benzmuller, Christoph" sort="Benzmuller, Christoph" uniqKey="Benzmuller C" first="Christoph" last="Benzmüller">Christoph Benzmüller</name><affiliation wicri:level="2"><country xml:lang="fr">États-Unis</country><wicri:regionArea>Articulate Software, Angwin, CA</wicri:regionArea><placeName><region type="state">Californie</region></placeName></affiliation><affiliation></affiliation></author></analytic><monogr></monogr><series><title level="j">Annals of Mathematics and Artificial Intelligence</title><title level="j" type="abbrev">Ann Math Artif Intell</title><idno type="ISSN">1012-2443</idno><idno type="eISSN">1573-7470</idno><imprint><publisher>Springer Netherlands</publisher><pubPlace>Dordrecht</pubPlace><date type="published" when="2011-06-01">2011-06-01</date><biblScope unit="volume">62</biblScope><biblScope unit="issue">1-2</biblScope><biblScope unit="page" from="103">103</biblScope><biblScope unit="page" to="128">128</biblScope></imprint><idno type="ISSN">1012-2443</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">1012-2443</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Classical and non-classical logics</term><term>Classical higher-order logic</term><term>Higher-order automated theorem proving</term><term>Knowledge representation</term><term>Logic combinations</term><term>Quantified multimodal logics</term><term>Semantic embeddings</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Numerous classical and non-classical logics can be elegantly embedded in Church’s simple type theory, also known as classical higher-order logic. Examples include propositional and quantified multimodal logics, intuitionistic logics, logics for security, and logics for spatial reasoning. Furthermore, simple type theory is sufficiently expressive to model combinations of embedded logics and it has a well understood semantics. Off-the-shelf reasoning systems for simple type theory exist that can be uniformly employed for reasoning within and about embedded logics and logics combinations. In this article we focus on combinations of (quantified) epistemic and doxastic logics and study their application for modeling and automating the reasoning of rational agents. We present illustrating example problems and report on experiments with off-the-shelf higher-order automated theorem provers.</div></front></TEI><affiliations><list><country><li>États-Unis</li></country><region><li>Californie</li></region></list><tree><country name="États-Unis"><region name="Californie"><name sortKey="Benzmuller, Christoph" sort="Benzmuller, Christoph" uniqKey="Benzmuller C" first="Christoph" last="Benzmüller">Christoph Benzmüller</name></region></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002738 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 002738 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:66DC056FECD94BC479D88167A3E49EDD4002FF46
|texte= Combining and automating classical and non-classical logics in classical higher-order logics
}}
| This area was generated with Dilib version V0.6.33. |  |